\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, $L$:(IdLnk List), $T$:(Id$\rightarrow$Type).
\\[0ex]es{-}secret{-}server\=\{table:ut2, encrypt:ut2, decrypt:ut2\}\+
\\[0ex](${\it es}$; $T$; $L$; $i$)
\-\\[0ex]$\Rightarrow$ \=($\forall$$e_{2}$, $e_{1}$:E.\+
\\[0ex](loc($e_{1}$) = $i$) $\Rightarrow$ ($e_{1}$ $<$loc $e_{2}$) $\Rightarrow$ (ptr(("table" after $e_{1}$)) $\leq$ ptr("table" when $e_{2}$)))
\-
\end{tabbing}